module sva_ca_property;

    logic clk;
    initial begin
        clk = 0;
        forever #5 clk = ~clk;
    end

    logic a, b, c, rst;

    initial begin
        rst=1; a=1; b=1; c=1; #5;  // 5ns
        rst=1; a=0; b=0; c=1; #10; // 15ns
        rst=1; a=1; b=0; c=1; #10; // 25ns
        rst=1; a=0; b=0; c=1; #10; // 35ns
        rst=0; a=1; b=1; c=1; #10; // 45ns
        rst=0; a=1; b=1; c=1; #10; // 55ns
        rst=0; a=0; b=1; c=1; #10; // 65ns
        rst=0; a=1; b=1; c=1; #10; // 75ns
        rst=0; a=0; b=1; c=1; #10; // 85ns
        rst=0; a=1; b=1; c=1; #10; // 95ns
        $finish;
    end

    // disable iff (rst) 的含义为: 当 rst 为真时终止属性检查
    property p;
        @(posedge clk) disable iff (rst) a |-> ##1 b[*3] ##1 c;
    endproperty

    cap1: assert property(p) $info("cap1 passed"); else $error("cap1 failed");

    initial begin
        $dumpfile("dump.vcd"); $dumpvars;
    end
endmodule
